p:PosetSig, a, b:|p|. (a < b)   

latex

Up	sets 1
Definitions of Statement	a < b
Definitions	x f y, a < b, t  T, x:A. B(x)
Lemmas	poset sig wf, set car wf, bnot wf, set le wf, band wf